Mattmüller et al. (2010) is a planner based on an adapted version of Hansen and Zilberstein (2001), a heuristic search algorithm that has theoretical guarantees to extract strong cyclic solutions for Markov decision problems. Kuter et al. (2008) makes use of Classical Planning algorithms to solve planning tasks. Fu et al. (2011) is similar to, but the main difference is that avoids exploring already explored/solved states, being more efficient than . Muise et al. (2012) is one the most efficient planners in the literature, and it is built upon some improvements over the state relevance techniques, such as avoiding dead-ends states. The main idea of these planners is selecting a reachable state s by the current policy that still is undefined in the current policy.

Fully observable non-deterministic (FOND) planning is becoming increasingly important as an approach for computing proper policies in probabilistic planning, extended temporal plans in LTL planning, and general plans in generalized planning. In this work, we introduce a SAT encoding for FOND planning that is compact and can produce compact strong cyclic policies. Simple variations of the encodings are also introduced for strong planning and for what we call, dual FOND planning, where some non-deterministic actions are assumed to be fair (e.g., probabilistic) and others unfair (e.g., adversarial). The resulting FOND planners are compared empirically with existing planners over existing and new benchmarks. The notion of "probabilistic interesting problems" is also revisited to yield a more comprehensive picture of the strengths and limitations of current FOND planners and the proposed SAT approach.

We create a unified framework for analyzing and synthesizing plans with loops for solving problems with non-deterministic numeric effects and a limited form of partial observability. Three different action models---with deterministic, qualitative non-deterministic and Boolean non-deterministic semantics---are handled using a single abstract representation. We establish the conditions under which the correctness and termination of solutions, represented as abstract policies, can be verified. We also examine the feasibility of learning abstract policies from examples. We demonstrate our techniques on several planning problems and show that they apply to challenging real-world tasks such as doing the laundry with a PR2 robot. These results resolve a number of open questions about planning with loops and facilitate the development of new algorithms and applications.